So, hallo, ich bin Selgi und wir wahrscheinlich schon gerettet haben, Herr Professor Schleuder kommt heute nicht und ich vertrete ihn.

Und der Thema für die heutige Vorlesung ist natürlich Schließen.

Mache ich neu.

Ja, ich schreibe sowieso heute nicht so viel, weil also mein Deutsch ist nicht so gut.

Wenn ich spreche, dann merkt man vielleicht mal nicht so sehr, aber wenn man schreibt, dann sieht man das gleich.

Bitte? Ah, na ja, ich kann das auf Englisch. Na ja, dann kenne ich die Fachworte nicht, also.

Also ich verwende gerne Formel als Worte.

Und also wir haben schon gesehen, diese natürliche Schließenkalkül für propositionelle Logik und würde ich sagen schon ganz viele Übungen gemacht.

Also das Brief soll schon mehr oder weniger klar sein.

Und natürlich ist es so gemeint, dass man einen Kalkül bekommt im Endeffekt für die ganze Logik 1. Stufe. Das war so ein Vorbereitensschritt für normale Logikoperation, für die Aussagenlogik.

Und was fällt noch ist die Quantorin natürlich. Wenn man die Quantoren reinschmeißt, dann kriegt man wirklich einen Kalkül für die Logik 1. Stufe.

Und das ist ja natürlich viel schöner, weil da kann man viele interessante Probleme formalisieren und beweisen.

Also ich erinnere kurz die Struktur von diesen natürlichen Schließenformeln oder Regeln. Da verwendet man so eine Duktion wie das zum Beispiel. A und B.

Das ist eine Schreibweise sozusagen und anders kann man das auch zuschreiben. A und B. Das ist hier was Voraussetzung.

Und das ist Konklusion. Oder generell ist es so. Also A1 bis AN als Annahmen.

B und das ist dasselbe als A1. Da schreibt man das ohne Komma. AN.

So zwei Notationen verwendet man und die sind also zwei Varianten von dasselbe. Das heißt normalerweise Fitch Style und das ist natürlich Schließen Style.

Und wie gesagt da fehlen noch irgendwelche Regeln und ich habe das schon gemerkt und vielleicht Herr Professor Schörl hat das ganz genau gesagt, dass jede Operation,

logische Operation kommt normalerweise mit zwei Typen von Regeln. Und zwar Einführungsregeln und Eliminationsregeln.

Und bei Quantoren ist es genauso. Wir haben zwei Quantoren. Al-Quantoren und Existenz-Quantoren. Aber wir brauchen natürlich nur ein Quantor,

weil den zweiten kann man dann einführen. Also als Basisfall kann man Al-Quantoren betrachten und dann kriegt man Existenz-Quantor nach Äquivalenz.

So wenn man Regeln hat für Al-Quantor, dann kann man also schon die vorlegerliche erste Stufe machen, weil die obere Formel kann man einfach reinkodieren und Existenz-Quantor gar nicht benutzen.

Also deswegen führe ich erstmal einen dieser Basisfall und dann zeige ich, wie kann man trotzdem auch die Regeln für Al-Quantoren, für Existenz-Quantoren auch einführen.

Also was heißt Syntaktik Sugar? Die braucht man nicht, aber das macht die Beweisen schöner und einfacher zu lesen.

Gut, dann fange ich mit einem kleinen Motivationbeispiel ein.

Das ist ein ganz, ganz bekanntes Beispiel und das ist ein Beispiel in einer natürlicher Sprache.

Also wir können sagen, Menschen sind sterblich.

Das ist einfach sozusagen.

Zum Beispiel Socrates ist ein Mensch und daraus kann man schließen, dass Socrates sterblich ist.

Ist das groß genug?

Gut.

Ja und wie kann man so eine schließen, logikerste Stufe formalisieren?

Also wir gehen davon aus, dass alle Elemente unserer Tagelmenge sind Menschen.

Das heißt, das ist unsere Annahme bei Formalisierung, das heißt, diese Fakt bedeutet, dass Socrates einfach zu einer Konstante ist.

Das entspricht keine richtigen Formeln.

Das bedeutet einfach, es gibt ein Symbol Socrates in der Signatur und sonst ist von Socrates nichts bekannt.

Aber das kann man schon wie eine Formel lesen und zwar wir können einen Prädikat einführen, sterblich oder einfach S.

Das ist ein Beispiel, das ich dazu schreibe.

Menschen sind sterblich bedeutet in dem Fall natürlich alle Menschen sind sterblich.

Also das ist ein Fall, wo wir Alkvantoren brauchen für alle x, s, x.

Das wie gesagt entspricht also keine Regel.

Und das ist die Konklusion.

Also so wird das Regel formalisiert und eigentlich sieht wirklich diese natürliche Schließenregel aus für Alkvantoren.

Und in.

Also.

Und das ist das ist anders.

Ja genau, wenn wir für alle x, phi haben, dann daraus folgt phi.

Cx.

Das heißt Alkontor Elimination.

So wenn für alle x, phi gilt, dann können wir diese x Variable in phi ersetzen mit einigen Ausdruck.